↳ Prolog
↳ PrologToPiTRSProof
perm_in(Xs, cons(X, Ys)) → U3(Xs, X, Ys, ap1_in(X1s, cons(X, X2s), Xs))
ap1_in(cons(H, X), Y, cons(H, Z)) → U1(H, X, Y, Z, ap1_in(X, Y, Z))
ap1_in(nil, X, X) → ap1_out(nil, X, X)
U1(H, X, Y, Z, ap1_out(X, Y, Z)) → ap1_out(cons(H, X), Y, cons(H, Z))
U3(Xs, X, Ys, ap1_out(X1s, cons(X, X2s), Xs)) → U4(Xs, X, Ys, X1s, X2s, ap2_in(X1s, X2s, Zs))
ap2_in(cons(H, X), Y, cons(H, Z)) → U2(H, X, Y, Z, ap2_in(X, Y, Z))
ap2_in(nil, X, X) → ap2_out(nil, X, X)
U2(H, X, Y, Z, ap2_out(X, Y, Z)) → ap2_out(cons(H, X), Y, cons(H, Z))
U4(Xs, X, Ys, X1s, X2s, ap2_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in(nil, nil) → perm_out(nil, nil)
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, cons(X, Ys))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
perm_in(Xs, cons(X, Ys)) → U3(Xs, X, Ys, ap1_in(X1s, cons(X, X2s), Xs))
ap1_in(cons(H, X), Y, cons(H, Z)) → U1(H, X, Y, Z, ap1_in(X, Y, Z))
ap1_in(nil, X, X) → ap1_out(nil, X, X)
U1(H, X, Y, Z, ap1_out(X, Y, Z)) → ap1_out(cons(H, X), Y, cons(H, Z))
U3(Xs, X, Ys, ap1_out(X1s, cons(X, X2s), Xs)) → U4(Xs, X, Ys, X1s, X2s, ap2_in(X1s, X2s, Zs))
ap2_in(cons(H, X), Y, cons(H, Z)) → U2(H, X, Y, Z, ap2_in(X, Y, Z))
ap2_in(nil, X, X) → ap2_out(nil, X, X)
U2(H, X, Y, Z, ap2_out(X, Y, Z)) → ap2_out(cons(H, X), Y, cons(H, Z))
U4(Xs, X, Ys, X1s, X2s, ap2_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in(nil, nil) → perm_out(nil, nil)
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, cons(X, Ys))
PERM_IN(Xs, cons(X, Ys)) → U31(Xs, X, Ys, ap1_in(X1s, cons(X, X2s), Xs))
PERM_IN(Xs, cons(X, Ys)) → AP1_IN(X1s, cons(X, X2s), Xs)
AP1_IN(cons(H, X), Y, cons(H, Z)) → U11(H, X, Y, Z, ap1_in(X, Y, Z))
AP1_IN(cons(H, X), Y, cons(H, Z)) → AP1_IN(X, Y, Z)
U31(Xs, X, Ys, ap1_out(X1s, cons(X, X2s), Xs)) → U41(Xs, X, Ys, X1s, X2s, ap2_in(X1s, X2s, Zs))
U31(Xs, X, Ys, ap1_out(X1s, cons(X, X2s), Xs)) → AP2_IN(X1s, X2s, Zs)
AP2_IN(cons(H, X), Y, cons(H, Z)) → U21(H, X, Y, Z, ap2_in(X, Y, Z))
AP2_IN(cons(H, X), Y, cons(H, Z)) → AP2_IN(X, Y, Z)
U41(Xs, X, Ys, X1s, X2s, ap2_out(X1s, X2s, Zs)) → U51(Xs, X, Ys, perm_in(Zs, Ys))
U41(Xs, X, Ys, X1s, X2s, ap2_out(X1s, X2s, Zs)) → PERM_IN(Zs, Ys)
perm_in(Xs, cons(X, Ys)) → U3(Xs, X, Ys, ap1_in(X1s, cons(X, X2s), Xs))
ap1_in(cons(H, X), Y, cons(H, Z)) → U1(H, X, Y, Z, ap1_in(X, Y, Z))
ap1_in(nil, X, X) → ap1_out(nil, X, X)
U1(H, X, Y, Z, ap1_out(X, Y, Z)) → ap1_out(cons(H, X), Y, cons(H, Z))
U3(Xs, X, Ys, ap1_out(X1s, cons(X, X2s), Xs)) → U4(Xs, X, Ys, X1s, X2s, ap2_in(X1s, X2s, Zs))
ap2_in(cons(H, X), Y, cons(H, Z)) → U2(H, X, Y, Z, ap2_in(X, Y, Z))
ap2_in(nil, X, X) → ap2_out(nil, X, X)
U2(H, X, Y, Z, ap2_out(X, Y, Z)) → ap2_out(cons(H, X), Y, cons(H, Z))
U4(Xs, X, Ys, X1s, X2s, ap2_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in(nil, nil) → perm_out(nil, nil)
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
PERM_IN(Xs, cons(X, Ys)) → U31(Xs, X, Ys, ap1_in(X1s, cons(X, X2s), Xs))
PERM_IN(Xs, cons(X, Ys)) → AP1_IN(X1s, cons(X, X2s), Xs)
AP1_IN(cons(H, X), Y, cons(H, Z)) → U11(H, X, Y, Z, ap1_in(X, Y, Z))
AP1_IN(cons(H, X), Y, cons(H, Z)) → AP1_IN(X, Y, Z)
U31(Xs, X, Ys, ap1_out(X1s, cons(X, X2s), Xs)) → U41(Xs, X, Ys, X1s, X2s, ap2_in(X1s, X2s, Zs))
U31(Xs, X, Ys, ap1_out(X1s, cons(X, X2s), Xs)) → AP2_IN(X1s, X2s, Zs)
AP2_IN(cons(H, X), Y, cons(H, Z)) → U21(H, X, Y, Z, ap2_in(X, Y, Z))
AP2_IN(cons(H, X), Y, cons(H, Z)) → AP2_IN(X, Y, Z)
U41(Xs, X, Ys, X1s, X2s, ap2_out(X1s, X2s, Zs)) → U51(Xs, X, Ys, perm_in(Zs, Ys))
U41(Xs, X, Ys, X1s, X2s, ap2_out(X1s, X2s, Zs)) → PERM_IN(Zs, Ys)
perm_in(Xs, cons(X, Ys)) → U3(Xs, X, Ys, ap1_in(X1s, cons(X, X2s), Xs))
ap1_in(cons(H, X), Y, cons(H, Z)) → U1(H, X, Y, Z, ap1_in(X, Y, Z))
ap1_in(nil, X, X) → ap1_out(nil, X, X)
U1(H, X, Y, Z, ap1_out(X, Y, Z)) → ap1_out(cons(H, X), Y, cons(H, Z))
U3(Xs, X, Ys, ap1_out(X1s, cons(X, X2s), Xs)) → U4(Xs, X, Ys, X1s, X2s, ap2_in(X1s, X2s, Zs))
ap2_in(cons(H, X), Y, cons(H, Z)) → U2(H, X, Y, Z, ap2_in(X, Y, Z))
ap2_in(nil, X, X) → ap2_out(nil, X, X)
U2(H, X, Y, Z, ap2_out(X, Y, Z)) → ap2_out(cons(H, X), Y, cons(H, Z))
U4(Xs, X, Ys, X1s, X2s, ap2_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in(nil, nil) → perm_out(nil, nil)
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
AP2_IN(cons(H, X), Y, cons(H, Z)) → AP2_IN(X, Y, Z)
perm_in(Xs, cons(X, Ys)) → U3(Xs, X, Ys, ap1_in(X1s, cons(X, X2s), Xs))
ap1_in(cons(H, X), Y, cons(H, Z)) → U1(H, X, Y, Z, ap1_in(X, Y, Z))
ap1_in(nil, X, X) → ap1_out(nil, X, X)
U1(H, X, Y, Z, ap1_out(X, Y, Z)) → ap1_out(cons(H, X), Y, cons(H, Z))
U3(Xs, X, Ys, ap1_out(X1s, cons(X, X2s), Xs)) → U4(Xs, X, Ys, X1s, X2s, ap2_in(X1s, X2s, Zs))
ap2_in(cons(H, X), Y, cons(H, Z)) → U2(H, X, Y, Z, ap2_in(X, Y, Z))
ap2_in(nil, X, X) → ap2_out(nil, X, X)
U2(H, X, Y, Z, ap2_out(X, Y, Z)) → ap2_out(cons(H, X), Y, cons(H, Z))
U4(Xs, X, Ys, X1s, X2s, ap2_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in(nil, nil) → perm_out(nil, nil)
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
AP2_IN(cons(H, X), Y, cons(H, Z)) → AP2_IN(X, Y, Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PiDP
AP2_IN(cons(X), Y) → AP2_IN(X, Y)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
AP1_IN(cons(H, X), Y, cons(H, Z)) → AP1_IN(X, Y, Z)
perm_in(Xs, cons(X, Ys)) → U3(Xs, X, Ys, ap1_in(X1s, cons(X, X2s), Xs))
ap1_in(cons(H, X), Y, cons(H, Z)) → U1(H, X, Y, Z, ap1_in(X, Y, Z))
ap1_in(nil, X, X) → ap1_out(nil, X, X)
U1(H, X, Y, Z, ap1_out(X, Y, Z)) → ap1_out(cons(H, X), Y, cons(H, Z))
U3(Xs, X, Ys, ap1_out(X1s, cons(X, X2s), Xs)) → U4(Xs, X, Ys, X1s, X2s, ap2_in(X1s, X2s, Zs))
ap2_in(cons(H, X), Y, cons(H, Z)) → U2(H, X, Y, Z, ap2_in(X, Y, Z))
ap2_in(nil, X, X) → ap2_out(nil, X, X)
U2(H, X, Y, Z, ap2_out(X, Y, Z)) → ap2_out(cons(H, X), Y, cons(H, Z))
U4(Xs, X, Ys, X1s, X2s, ap2_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in(nil, nil) → perm_out(nil, nil)
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
AP1_IN(cons(H, X), Y, cons(H, Z)) → AP1_IN(X, Y, Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
AP1_IN(cons(Z)) → AP1_IN(Z)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
PERM_IN(Xs, cons(X, Ys)) → U31(Xs, X, Ys, ap1_in(X1s, cons(X, X2s), Xs))
U31(Xs, X, Ys, ap1_out(X1s, cons(X, X2s), Xs)) → U41(Xs, X, Ys, X1s, X2s, ap2_in(X1s, X2s, Zs))
U41(Xs, X, Ys, X1s, X2s, ap2_out(X1s, X2s, Zs)) → PERM_IN(Zs, Ys)
perm_in(Xs, cons(X, Ys)) → U3(Xs, X, Ys, ap1_in(X1s, cons(X, X2s), Xs))
ap1_in(cons(H, X), Y, cons(H, Z)) → U1(H, X, Y, Z, ap1_in(X, Y, Z))
ap1_in(nil, X, X) → ap1_out(nil, X, X)
U1(H, X, Y, Z, ap1_out(X, Y, Z)) → ap1_out(cons(H, X), Y, cons(H, Z))
U3(Xs, X, Ys, ap1_out(X1s, cons(X, X2s), Xs)) → U4(Xs, X, Ys, X1s, X2s, ap2_in(X1s, X2s, Zs))
ap2_in(cons(H, X), Y, cons(H, Z)) → U2(H, X, Y, Z, ap2_in(X, Y, Z))
ap2_in(nil, X, X) → ap2_out(nil, X, X)
U2(H, X, Y, Z, ap2_out(X, Y, Z)) → ap2_out(cons(H, X), Y, cons(H, Z))
U4(Xs, X, Ys, X1s, X2s, ap2_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in(nil, nil) → perm_out(nil, nil)
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
PERM_IN(Xs, cons(X, Ys)) → U31(Xs, X, Ys, ap1_in(X1s, cons(X, X2s), Xs))
U31(Xs, X, Ys, ap1_out(X1s, cons(X, X2s), Xs)) → U41(Xs, X, Ys, X1s, X2s, ap2_in(X1s, X2s, Zs))
U41(Xs, X, Ys, X1s, X2s, ap2_out(X1s, X2s, Zs)) → PERM_IN(Zs, Ys)
ap1_in(cons(H, X), Y, cons(H, Z)) → U1(H, X, Y, Z, ap1_in(X, Y, Z))
ap1_in(nil, X, X) → ap1_out(nil, X, X)
ap2_in(cons(H, X), Y, cons(H, Z)) → U2(H, X, Y, Z, ap2_in(X, Y, Z))
ap2_in(nil, X, X) → ap2_out(nil, X, X)
U1(H, X, Y, Z, ap1_out(X, Y, Z)) → ap1_out(cons(H, X), Y, cons(H, Z))
U2(H, X, Y, Z, ap2_out(X, Y, Z)) → ap2_out(cons(H, X), Y, cons(H, Z))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
U41(ap2_out(Zs)) → PERM_IN(Zs)
PERM_IN(Xs) → U31(ap1_in(Xs))
U31(ap1_out(X1s, cons(X2s))) → U41(ap2_in(X1s, X2s))
ap1_in(cons(Z)) → U1(ap1_in(Z))
ap1_in(X) → ap1_out(nil, X)
ap2_in(cons(X), Y) → U2(ap2_in(X, Y))
ap2_in(nil, X) → ap2_out(X)
U1(ap1_out(X, Y)) → ap1_out(cons(X), Y)
U2(ap2_out(Z)) → ap2_out(cons(Z))
ap1_in(x0)
ap2_in(x0, x1)
U1(x0)
U2(x0)
PERM_IN(Xs) → U31(ap1_in(Xs))
POL(PERM_IN(x1)) = 2 + 2·x1
POL(U1(x1)) = 1 + x1
POL(U2(x1)) = 2 + x1
POL(U31(x1)) = 2·x1
POL(U41(x1)) = 2 + x1
POL(ap1_in(x1)) = x1
POL(ap1_out(x1, x2)) = x1 + x2
POL(ap2_in(x1, x2)) = 2·x1 + 2·x2
POL(ap2_out(x1)) = 2·x1
POL(cons(x1)) = 1 + x1
POL(nil) = 0
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ DependencyGraphProof
U41(ap2_out(Zs)) → PERM_IN(Zs)
U31(ap1_out(X1s, cons(X2s))) → U41(ap2_in(X1s, X2s))
ap1_in(cons(Z)) → U1(ap1_in(Z))
ap1_in(X) → ap1_out(nil, X)
ap2_in(cons(X), Y) → U2(ap2_in(X, Y))
ap2_in(nil, X) → ap2_out(X)
U1(ap1_out(X, Y)) → ap1_out(cons(X), Y)
U2(ap2_out(Z)) → ap2_out(cons(Z))
ap1_in(x0)
ap2_in(x0, x1)
U1(x0)
U2(x0)